Left Termination
of the query pattern
gtsolve(g,a)
w.r.t. the given
Prolog program
could successfully be
proven
:
0 Prolog
↳
1 PrologToPrologProblemTransformerProof (⇒, 0 ms)
↳
2 TRUE
(0)
Obligation:
Clauses:
gtsolve
(
X
,
Y
) :-
','
(
generate
(
X
,
Y
),
test
(
Y
)).
Query: gtsolve(g,a)
(1) PrologToPrologProblemTransformerProof (SOUND transformation)
Built Prolog problem from termination graph ICLP10.
digraph dp_graph { node [outthreshold=100, inthreshold=100]; 1 [label="1: gtsolve(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red]; 2 [label="2: gtsolve(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow]; 3 [label="3: ','(generate(T5, T7), test(T7))\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow]; 4 [label="4: \n\n", fontsize=16, style=filled, fillcolor=lightyellow]; 5 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan]; 1 -> 5 [arrowhead = none ]; 5 -> 2; 6 [label="ONLY EVAL with clause\ngtsolve(X3, X4) :- ','(generate(X3, X4), test(X4)).\nand substitutionT1 -> T5,\nX3 -> T5,\nT2 -> T7,\nX4 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue]; 2 -> 6 [arrowhead = none ]; 6 -> 3; 7 [label="UNDEFINED ERROR", fontsize=14, style = filled, fillcolor = lightgreen]; 3 -> 7 [arrowhead = none ]; 7 -> 4; }
(2)
TRUE